Inference at * 1 3 1 0 1 1 2 
Iof proof for Lemma fincr wf:

.....wf..... NILNIL

1. P : 
2. j:. (k:. (k < j)  (P(k)))  (P(j))
    Type 

latex

 by MemEqCD 

latex

 .

Definitions	Type, f(a), a < b, P  Q, x:A. B(x), , x:AB(x), , s = t, t  T
Lemmas	nat wf